00100	SU-AI
00200	
00300	
00400	Artificial Intelligence Project
00500	Computer Science Department
00600	Stanford University
00700	Stanford, California 94305
00800	PDP-10 and PDP-6
00900	
01000	I. Personnel
01100	
01200	Director - John McCarthy
01300	
01400	Executive Officer - Lester Earnest	x4202
01500	Associate Director- Jerome Feldman	x4532
01600	NIC Station Agent - Barbara Barnett	x2800
01700	Network Software - Andy Moorer		x4971	JAM
01800	
01900	II. Installation Type
02000	
02100		The computer system includes PDP-10 and PDP-6 processors,
02200	256K of core, a swapping disk, an IBM 3330 for file storage including
02300	a user disk pack, IBM compatible 7 channel tape, Dectape, about 40
02400	keyboard-display terminals, and i-o equipment for robotics research
02500	including TV cameras, arms, and a cart.  The system software is a
02600	modified version of the D.E.C. system for the PDP-10.  The major
02700	languages used are the FAIL symbolic assembler, the SAIL algebraic
02800	compiler, LISP, and micro-PLANNER.
02900	
03000	
03100	VI. Interests and capabilities.
03200	
03300		The Stanford Artificial Intelligence Laboratory has potential
03400	interest in all areas of AI and mathematical theory of computation.  The
03500	following activities a receiving significant effort at present:
03600	
03700		1. Computer vision.  Edge finding, body and scene description,
03800	use of color, parallax, and controlled illumination.  If and when the
03900	it is feasible to transmit pictures over the network, network collaboration
04000	in this area may become feasible.
04100	The leaders of this work are Jerry Feldman (JAF) and Tom Binford (TOB).
04200	
04300		2. Robotics.  Projects in arm control and control of a vehicle
04400	are in progress.  Feldman and Binford are in charge here too.
04500	
04600		3. Mathematical Theory of Computation.  The group in this area
04700	includes John McCarthy, Robin Milner, Richard Weyhrauch, Ralph London,
04800	Shigeru Igarashi, and David Luckham and Whitfield Diffie.  Two programs
04900	for checking mathematical proofs may be of interest to network users.
05000	The first checks proofs in predicate calculus, and Diffie (WD) is
05100	responsible for it.  The second which checks proofs in version of
05200	Scott's logic is in the charge of Milner (RGM) and Weyhrauch (RWW).
05300	Both programs have been used for checking the proofs of correctness
05400	of computer programs.  Network use of these programs (at least
05500	experimentally) is probably quite feasible.
05600	
05700		4. Computer theorem proving.  Luckham (DCL) has a resolution
05800	theorem prover of considerable power as such things go.  Its experimental
05900	network 
06000	use is probably also feasible.
06100	
06200		5. Arthur Samuel (ALS) heads our speech recognition work.
06300	There may be some network interest in our speech programs.
06400	
06500		6. There is a project for a new version of LISP called LISP 70.
06600	Experimental versions will be available in the summer of 1972, and
06700	information may be obtained from Horace Enea (HJE), Dave Smith (DCS)
06800	or Larry Tesler (TES).
06900	
07000		7. Yorick Wilks (YAW) is writing programs for translating
07100	between English and French.
07200	
07300		Apart from the research work in AI and MTC, there may be some
07400	interest in our system software.  Specifically, other installations
07500	may be interested in experimenting with the FAIL assembler which is
07600	very fast, the SAIL compiler which is ALGOL + LEAP structures, or
07700	our editor SOS.  Inquiries about documentation should be directed to
07800	Barbara Barnett (BB) or Marilyn Mullins (MLM).